User blog:TheKing44/Ordinal Definable System of Fundamental Sequences
For the purposes of this post, I will be working in the set theory ZF unless otherwise stated. I will define an exceedingly strong system of fundamental sequences. In particular it will be the strongest system of fundamental sequences definable in first order set theory. This is useful since strong systems of fundamental sequences are needed for using the fast-growing hierarchy. Let \alpha be a countable limit ordinal such that there exists an ordinal definable bijection between \alpha and \mathbb N .The class of ordinal definable sets is well orderable. Moreover, we can *define* a specific well ordering. First, we well ordinal the set of formulas with ordinal parameters. We use shortlex order over the formulas, with ordinal parameters following the symbols of first order set theory in the language. (EDIT: After writing this post, I realized this ordering will make the resulting system a pain in the butt to analyze. It is still correct, but further analysis would be unnecessarily difficult. To make it a little easier, the ordering over formulas first compares the largest ordinal parameter each formula uses, and then uses the shortlex to break ties.) Now, we compare two ordinal definable sets by comparing there earliest defining formulas. This well orders the ordinal definable sets. Now, let f_\alpha be the earliest ordinal definable bijection between \alpha and \mathbb N according to the well ordering defined above. f_\alpha can be interpreted as a sequence of ordinals. We remove from this sequence any ordinal which follows a larger ordinal, to create s_\alpha . s_\alpha is increasing since we removed all the ordinals that followed a larger ordinal. Moreover, its supremum equals \alpha , since otherwise the supremum+1 was removed from the sequence, implying that an ordinal larger than the supremum+1 was in the sequence, which is contradictory since than s would contain an element larger than its supremum. These f s make up our system of fundamental sequences. I call it the ordinal definable system of fundamental sequences (odsfs). Is this a system of fundamental sequences? Well, if \alpha is in it, then so will any smaller limit ordinal \beta . That's because we can treat f_\alpha as a sequence, remove all the ordinals that are not less than \beta , and use that to define a bijection between \beta and \mathbb N . Since f_\alpha is ordinal definable, and the only parameter we added is an ordinal, this bijection will be ordinal definable. So, how powerful is this system? Well, if V=OD (a statement which is independent of ZF, or even ZFC), then it includes every countable ordinal! In ZFC, it is well known that a system of fundamental sequences including every countable limit ordinal exists, but usually a specific example is not given (or is impossible to give). Odsfs on the other hand is a specific example! If we do not assume V=OD, we still have something pretty special. Metatheortically, since ordinal definability is definable in first-order set theory, the system of f s is definable in first-order set theory. However, no other system of fundamental sequences definable in first order set theory could include a limit ordinal \alpha that odsfs does not, since then \alpha 's fundamental sequence in that system would be ordinal definable, contradicting the fact that is not in odsfs. So, odsfs is the most powerful system of fundamental sequences definable in first-order set theory (and therefore the most powerful explicit example you could work with in ZF or ZFC)! P.S. The supremum of the domain of odsfs should probably be called \omega_1^{\text{HOD}} since HOD thinks it is \omega_1 . You can't add it to odsfs because even though it is definable, none of its fundamental sequences are. Category:Blog posts